<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" 
          "http://www.w3.org/TR/html4/strict.dtd">
<!-- Material used from: HTML 4.01 specs: http://www.w3.org/TR/html401/ -->
<html>
<head>
  <META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
  <title>KLEE - Tutorial One</title>
  <link type="text/css" rel="stylesheet" href="menu.css">
  <link type="text/css" rel="stylesheet" href="content.css">
</head>
<body>
<!--#include virtual="menu.html.incl"-->
<div id="content">
  <!--*********************************************************************-->
  <h1>Tutorial One: Testing a Small Function</h1>
  <!--*********************************************************************-->
  
  <h2>The demo code</h2>

  This tutorial walks you through the main steps needed to test a
  simple function with KLEE.  Here is our simple function:

  <pre class="code">
  int my_islower(int x) {
      if (x >= 'a' && x <= 'z')  
         return 1;
      else return 0;
  } </pre>

  You can find the entire code for this example in the source tree
  under <tt>examples/islower</tt>.  A version of the source code can
  also be accessed <a href="resources/islower.c.html">here</a>. 

  <h2>Marking input as symbolic</h2> 

  In order to test this function with KLEE, we need to run it
  on <i>symbolic</i> input.  To mark a variable as symbolic, we use
  the <tt>klee_make_symbolic()</tt> function, which takes three
  arguments: the address of the variable (memory location) that we
  want to treat as symbolic, its size, and a name (which can be
  anything).  Here is a simple <tt>main()</tt> function that marks a
  variable <tt>c</tt> as symbolic and uses it to
  call <tt>my_islower()</tt>:

  <pre class="code">
  int main() {
      char c;
      klee_make_symbolic(&c, sizeof(c), "input"); 
      return my_islower(c);
  } </pre>
		


  <h2>Compiling to LLVM bitcode</h2>

  KLEE operates on LLVM bitcode.  To run a program with KLEE, you
  first compile it to LLVM bitcode using <tt>llvm-gcc
  --emit-llvm</tt>.  Assuming our code is stored in <tt>demo.c</tt>,
  we run:

  <div class="instr">
  llvm-gcc --emit-llvm -c -g demo.c
  </div>

  to generate the LLVM bitcode file <tt>demo.o</tt>.

  It is useful to (1) build with <tt>-g</tt> to add debug information
  to the bitcode file, which we use to generate source line level
  statistics information, and (2) not use any optimization flags.  The
  code can be optimized later, as KLEE provides the
  <tt>--optimize</tt> command line option to run the optimizer
  internally.
    
  <h2>Running KLEE</h2>
      
  To run KLEE on the bitcode file simply execute:
  
  <div class="instr">
  klee demo.o
  </div>

  You should see the following output:
  <pre class="output">
  KLEE: output directory = "klee-out-0"
  KLEE: done: total instructions = 69  
  KLEE: done: completed paths = 3      
  KLEE: done: generated tests = 3 </pre>

  There are three paths through our simple function, one
  where <tt>x</tt> is less than <tt>'a'</tt>, one where <tt>x</tt> is
  between <tt>'a'</tt> and <tt>'z'</tt> (so it's a lowercase letter),
  and one where <tt>x</tt> is greater than <tt>'z'</tt>.

  As expected, KLEE informs us that it explored three paths in the
  program and generated one test case for each path explored.  The
  output of a KLEE execution is a directory (in our
  case <tt>klee-out-0</tt>) containing the test cases generated by
  KLEE.  KLEE names the output directory <tt>klee-out-N</tt> where N
  is the lowest available number (so if we run KLEE again it will
  create a directory called <tt>klee-out-1</tt>), and also generates a
  symbolic link called <tt>klee-last</tt> to this directory for
  convenience:

  <pre class="output">
  $ ls klee-last/
  assembly.ll      run.istats       test000002.ktest
  info             run.stats        test000003.ktest
  messages.txt     test000001.ktest warnings.txt </pre>

  Please click <a href="klee-files.html">here</a> if you would like an
  overview of the files generated by KLEE.  In this tutorial, we only
  focus on the actual test files generated by KLEE.

  <h2>KLEE-generated test cases</h2> The test cases generated by KLEE
  are written in files with extension <tt>.ktest</tt>.  These are
  binary files, which can be read with the <tt>ktest-tool</tt>
  utility.  So let's examine each file:

  <pre class="output">
  $ ktest-tool klee-last/test000001.ktest 
  ktest file : 'klee-last/test000001.ktest'
  args       : ['demo.o']
  num objects: 1
  object    0: name: 'input'
  object    0: size: 1
  object    0: data: 'b'

  $ ktest-tool klee-last/test000002.ktest 
  ...
  object    0: data: '~'

  $ ktest-tool klee-last/test000003.ktest 
  ..
  object    0: data: '\x00' </pre>

  In each test file, KLEE reports the arguments with which the program
  was invoked (in our case no arguments other than the program name
  itself), the number of symbolic objects on that path (only one in
  our case), the name of our symbolic object ('input') and its size
  (1).  The actual test itself is represented by the value of our
  input: <tt>'b'</tt> for the first test, <tt>'~'</tt> for the second
  and <tt>0</tt> for the last one.  As expected, KLEE generated a
  character which is a lowercase letter (<tt>'b'</tt>), one which is
  less than <tt>'a'</tt> (<tt>0</tt>), and one which is greater
  than <tt>'z'</tt> (<tt>'~'</tt>).  We can now run these values on a
  native version of our program, to exercise all paths through the
  code!
 

  <h2>Replaying a test case</h2> 

  While we can run the test cases generated by KLEE on our program by
  hand, (or with the help of an existing test infrastructure), KLEE
  provides a convenient <i>replay library</i>, which simply replaces
  the call to <tt>klee_make_symbolic</tt> with a call to a function
  that assigns to our input the value stored in the <tt>.ktest</tt>
  file.

  To use it, simply link your program with the <tt>libkleeRuntest</tt>
  library and set the <tt>KTEST_FILE</tt> environment variable to
  point to the name of the desired test case:

  <pre class="output">
  $ gcc ~/klee/Release/lib/libkleeRuntest.dylib demo.c
  $ KTEST_FILE=klee-last/test000001.ktest ./a.out 
  $ echo $?
  1
  $ KTEST_FILE=klee-last/test000002.ktest ./a.out 
  $ echo $?
  0
  $ KTEST_FILE=klee-last/test000003.ktest ./a.out
  $ echo $?
  0 </pre>

  As expected, our program returns 1 when running the first test case
  (which contains the lowercase letter <tt>'b'</tt>), and 0 when
  running the other two (which don't contain lowercase letters).

  <br/><br/>

</div>
</body>
</html>
